The geometry of interaction (GoI) was introduced by Jean-Yves Girard shortly after his work on Linear Logic. In linear logic, proofs can be seen as some kind of networks instead of the flat tree structure of sequent calculus. To distinguish the real proof nets from all the possible networks, Girard devised a criterium involving trips in the network. Trips can in fact be seen as some kind of operator acting on the proof. Drawing from this observation, Girard described directly this operator from the proof and has given a formula, the so-called execution formula, encoding the process of cut elimination at the level of operators.
At the same time, Lamping had given a hard to understand algorithm to compute the optimal reduction strategy for the lambda calculus. Gonthier, Abadi and Levy have further shown that GoI allows better analysis of Lamping's algorithm. This work on the lambda calculus has been independently carried by Danos and Regnier, Asperti and Guerrini. GoI work had a strong influence on game semantics for linear logic and PCF.
GoI has been applied by Mackie to deep compiler optimisation for lambda calculi. A bounded version of GoI dubbed the Geometry of Synthesis has been used by Ghica to compile higher-order programming languages directly into static circuits.